ePMC

Benchmark

Model:	coupon v.1 (DTMC)
Parameter(s)	N = 9, DRAWS = 4, B = 5
Property:	exp_draws (exp-reward)

Invocation (default)

java -Xms10240m -Xmx10240m -jar ./root/epmc-standard.jar check --model-input-files coupon.9-4.jani --model-input-type jani --property-input-names exp_draws --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const B=5

Execution

Walltime:	2.2164459228515625s
Return code:	0
Note(s):	The tool result 'Infinity' is tagged as incorrect. The reference result is '112175240050457/16643031685280' (approx. 6.74007249230144) which means a relative error of 'inf' which is larger than the goal precision '0.001'.
Relative Error:	inf

Log

assertions-disabled
model-checking
analysing-property exp_draws
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-done 1 0
iterating
iterating-done 1 0
num-states-in-filter 1 "initial"
printing-all-filter-results
print-filter 0 0 Infinity
model-checking-done 0
command-check-result-is Infinity exp_draws